f:Top, T:Type, L:T List, i:||L||. map(f;L)[i] ~ (f(L[i])) 

latex

Definitions	t  T, x:A. B(x), ||as||, {i..j}, Top, P  Q, False, A, P & Q, AB, i  j < k, hd(l), i<j, ij, l[i], {T}, SQType(T), Prop, P  Q, Dec(P), True, b, b, , T, P  Q, P  Q, Unit, tl(l)
Lemmas	eqtt to assert, assert of le int, iff transitivity, eqff to assert, squash wf, true wf, bnot of le int, assert of lt int, le int wf, bool wf, le wf, lt int wf, assert wf, bnot wf, decidable int equal, top wf, int seg wf, length wf1